$\forall$$T$:Type, $Q$:(($T$ List)$\rightarrow$Prop).
\\[0ex]$Q$(nil) $\Rightarrow$ ($\forall$${\it ys}$:$T$ List, $y$:$T$. $Q$(${\it ys}$) $\Rightarrow$ $Q$(${\it ys}$ @ [$y$])) $\Rightarrow$ \{$\forall$${\it zs}$:$T$ List. $Q$(${\it zs}$)\}